(declare-const v0 Bool)
(declare-const v5 Bool)
(declare-const i1 Int)
(declare-const i3 Int)
(push)
(assert (= (distinct (< i3 14) true) true true (=> v5 v0) true true true true true true))
(assert (>= i1 (+ i3 i3 (abs i1) (abs i1))))
(check-sat)
(pop)
(assert (not (distinct i3 81)))
(check-sat)
